loc:Id, ds:fpf(Id; x.Type), knd:Knd, T:Type, x:Id,
f:((decl-state(ds)Tdecl-type{i:l}
f:((decl-state(ds)Tdecl-type(ds; x)) + (decl-state(ds)Trationalsdecl-type{i:l}
f:((decl-state(ds)Tdecl-type(ds; x)) + (decl-state(ds)Trationalsdecl-type(ds; x))).
Reffect(loc; ds; knd; T; x; f)  es_realizer{i:l} 

latex

Definitions	x. t(x), Reffect(loc; ds; knd; T; x; f), es_realizer{i:l}, t  T, x:A. B(x), x(s)
Lemmas	fpf wf, Id wf, unit wf, bool wf, finite-prob-space wf, IdLnk wf, decl-state wf, Knd wf, rationals wf, decl-type wf